/*
 * 
 */
package milecToMinisat;

import java.util.LinkedList ;
import java.io.PrintStream ;
import util.* ;


/** 
 * This is the traduction part of the milecToMinisat package. This class 
 * (should) implements the interface ClauseGenerator
 * and generate  a minisat+ interpretable programs from call
 *  to the abstract syntax described in the interface ClauseGenerator
 *  
 * @author ter-topcased-ups
 * @version 0.01, 2008/12/03
 * @see 
 */
public class Converter {

	static private Converter instance ;
	
	private int counterTmp ;
	private int counterNbr  ;
	private LinkedList<String> goal ; // the min: line
	private util.StringOutputStream clauses ;
	private PrintStream printStreamOnClauses ;
	
	
	/*pattern singleton */
	static public Converter getInstance() {
		if ( instance == null)
			instance = new Converter() ;
		return instance ;
	}
	
	Converter() {		
		initialize() ;
	}
		
	private void initialize() {
		goal = new LinkedList<String>() ;
		clauses = new util.StringOutputStream() ;
		printStreamOnClauses = new PrintStream(clauses) ;
		counterTmp = 0 ;
		counterNbr = 0 ;
	}
	
	/**
	 * get an unused yet id for a temporary variable.
	 * @return this id
	 */
	int getTmpId() {
		return counterTmp++ ;
	}
	
	/**
	 * get an unused yet id for a number variable.
	 * @return this id
	 */
	int getNbrId() {
		return counterNbr ++;
	}
	
	/**
	 * minisat clauses generated by the converter. 
	 */
	String getClauses() {
		return clauses.toString() ;
	}
	
	
	/**
	 * 
	 * @param val
	 * @param nbrBit
	 * @param stream
	 * @return
	 */
	int genIntegerConstant(int val,int nbrBit)
	{
		//TODO  clean methode (enlever commentaires de suivi)
		
		// on prend un identifiant unique pour le nombre
		int id = getNbrId() ;
		
		//on convertit l'entier en bits
		String binaire = Integer.toBinaryString(val) ;	
		int i = nbrBit - 1 ;
		
		/* si le nombre en bits est plus court que la taille souhaitee, 
		 * on complete avec des 0.*/
		for (  ; i > binaire.length()-1 ; i -- ) {
			printStreamOnClauses.print("nbr"+id+'b'+i+" = 0 ;\n" ) ;
		}
		/*on definit les bits trouves precedemment*/
		for (  ; i >= 0 ; i -- ) {
			printStreamOnClauses.print("nbr"+id+'b'+i+" = "
					+binaire.charAt(binaire.length()-i-1)+" ;\n" ) ;
		}
		return id ;
	}
	
	/** 
	 * @deprecated  replaced by {@link #printNumberAsSequenceOfBits(IntegerVariable,String)}
	 */
	private void printNumberAsSumOfBits(IntegerVariable var) {
		printNumberAsSequenceOfBits(var,"+") ;
	}
	
	/**
	 * write a variable as the sum (or minus the sum) of bits weighted
	 * with power of two
	 * <p>
	 * Example :
	 * <p>
	 * <code>
	 * printNumberAsSequenceOfBits(new IntegerVariable("x",10),"+") ;
	 * </code>
	 * <p>
	 * will write
	 * <p>
	 * <code>+1*x0 +2*x1 +4*x2 +8*x3</code>
	 * @param var
	 * @param sign "+" or "-"
	 */
	private void printNumberAsSequenceOfBits(IntegerVariable var,String sign) {
		int puissance2 = 1 ;	
		for (int i = 0 ; i < var.getSize(); i++) {
			printStreamOnClauses.print(sign+puissance2+"*"+var.name+"b"+i+" ") ;
			puissance2 *= 2 ;
		}
	}	
	
	public void genIntegerConstraint( IntegerVariable var , IntegerConstraintType constraintType,IntegerCst cst)  {
		printNumberAsSumOfBits(var) ;
		printStreamOnClauses.print(constraintType.getMinisatSymbol() +" " ) ;
		printStreamOnClauses.print(cst.getValue()) ;
		printStreamOnClauses.print(" ;\n") ;		
	}
	
	public void genIntegerCalc (IntegerOperation intOp,IntegerExp finalLeft, IntegerExp finalRight, IntegerVariable tmp) {
		intOp.getOp().genIntegerOp((IntegerVariable)finalLeft,(IntegerVariable)finalRight,tmp) ;
	}
	
	
	public void genIntegerAdd(IntegerVariable finalLeft , IntegerVariable finalRight,  IntegerVariable tmp) {
			printNumberAsSequenceOfBits((IntegerVariable)finalLeft,"+") ;
			printNumberAsSequenceOfBits((IntegerVariable)finalRight,"+") ;
			printNumberAsSequenceOfBits(tmp,"-") ;
			printStreamOnClauses.print(" = 0 ;\n") ;			
		}
	
	public void genIntegerSub(IntegerVariable finalLeft , IntegerVariable finalRight,  IntegerVariable tmp)  {
			printNumberAsSequenceOfBits((IntegerVariable)finalLeft,"+") ;
			printNumberAsSequenceOfBits((IntegerVariable)finalRight,"-") ;
			printNumberAsSequenceOfBits(tmp,"-") ;
			printStreamOnClauses.print(" = 0 ;\n") ;	
	}
	
	public void genIntegerMul(IntegerVariable finalLeft , IntegerVariable finalRight,  IntegerVariable tmp) {

		int productId = getTmpId() ;
		for (int i = 0 ; i < finalLeft.getSize() ; i ++) {
			for (int j = 0 ; j < finalRight.getSize() ; j++) {
				genBooleanAnd(finalLeft.name, finalRight.name, "tmp"+productId+"i"+i+"j"+j) ;
			}
		}
		for (int i = 0 ; i < finalLeft.getSize() ; i ++) {
			for (int j = 0 ; j < finalRight.getSize() ; j++) {
				printStreamOnClauses.print("+"+MathPerso.pow(2,i+j)+"*tmp"+productId+"i"+i+"j"+j+" ") ;
			}
		}
		printNumberAsSequenceOfBits(tmp,"-") ;
		printStreamOnClauses.print(" = 0 ;\n") ;	
	}
	
	public void genIntegerDiv(IntegerVariable finalLeft , IntegerVariable finalRight,  IntegerVariable tmp) {
		//TODO division entier
		IntegerVariable t = IntegerVariable.tempVar(IntegerOperator.multiplication.getSize(finalRight, tmp)) ;
		IntegerVariable r = IntegerVariable.tempVar(finalRight.getSize()) ;
		ClauseGeneratorImpl.getInstance().addIntegerConstraint(
				new IntegerOperation(
						t ,
						IntegerOperator.subtraction,
						new IntegerOperation(
								finalRight,
								IntegerOperator.multiplication,
								tmp )
						) ,
				IntegerConstraintType.equal, 
				new IntegerCst(0)
				) ;
		ClauseGeneratorImpl.getInstance().addIntegerConstraint(
				new IntegerOperation(
						finalLeft,
						IntegerOperator.subtraction,
						new IntegerOperation(
								t,
								IntegerOperator.addition,
								r )
					),
				IntegerConstraintType.equal, 
				new IntegerCst(0)
				) ;	
			ClauseGeneratorImpl.getInstance().addIntegerConstraint(
					new IntegerOperation(
							finalRight,
							IntegerOperator.subtraction,
							r),
					IntegerConstraintType.greater,
					new IntegerCst(0)
					) ;
		}
	
	public void genIntegerMod(IntegerVariable finalLeft , IntegerVariable finalRight,  IntegerVariable tmp) {
		//TODO modulo entier
		}
	
	public void genBooleanAnd(String x,String y, String z) {
		printStreamOnClauses.println("-1*"+x+" -1*"+y+" +1*"+z+" >=-1 ;") ;
		printStreamOnClauses.println("+1*"+x+" -1*"+z+" >= 0 ;") ;
		printStreamOnClauses.println("+1*"+y+" -1*"+z+" >= 0 ;") ;
	}
	
	}
	
